es:ES, A:Type, ds:x:Id fp Type, conds_list:(k:Knd fp V:Type  (State(ds)V(A + Top)) List),
i:Id.
(condsconds_list. es-triggers-params-consistent(es;A;i;ds;conds))
 (conds1,conds2conds_list.  conds1 || conds2)
 (p-first(map(conds.es-triggers(es;i;ds;conds);conds_list))
 (=
 (es-triggers(es;i;ds;(conds_list))
 ( AbsInterface(A)) 

latex

Definitions

x:A. B(x), t  T, x. t(x), map(f;as), (L), reduce(f;k;as), Y, P  Q, (x,yL.  P(x;y)), , A  B, A, False, P  Q, P & Q, x:A. B(x), P  Q, b, e  X, if b then t else f fi , ff, es-triggers(es;i;ds;conds), , can-apply(f;x), p  q, x  dom(f), deq-member(eq;x;L), t.1, isl(x), x,y. t(x;y), a:A fp B(a), Knd, AbsInterface(A), A c B, (x  l), SQType(T), {T}, Top, S  T, es-triggers-params-consistent(es;A;i;ds;conds), xL. P(x), f || g, T, True, mapl(f;l), x(s), {i..j}, i  j < k, ||as||, x(s1,s2), , Dec(P), P  Q, null(as), tt

Lemmas

fpf wf, Knd wf, decl-state wf, top wf, Id wf, event system wf, int seg wf, length wf2, fpf-compatible wf, Kind-deq wf, select wf, l all wf2, es-triggers-params-consistent wf, l member wf, es-is-interface wf, p-first wf-interface, es-interface wf, es-interface-extensionality, es-triggers wf, fpf-empty wf, assert wf, fpf-dom wf, es-kind wf, es-loc wf, es-E wf, bfalse wf, pairwise wf, l all cons, pairwise-cons, p-first-cons, mapl wf, nat wf, length wf1, IdLnk wf, Id sq, es-triggers-conditional, fpf-join-list wf, decidable assert, null wf3, es-triggers-params-list-join, fpf-empty-compatible-right, fpf-trivial-subtype-top, fpf-ap wf, fpf-join wf, fpf-compatible-join, implies functionality wrt iff, p-conditional wf, squash wf, true wf